$\forall$$a$:Id, $T$:Type, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:Top, $x$:Id, $L$:Top, $t$:Type.
\\[0ex]${\it ds}$ $\parallel$ $x$ : $t$
\\[0ex]$\Rightarrow$ (only members of $L$ affect $x$ :$t$ $\Vert\!+$ (with ds: ${\it ds}$ action $a$:$T$ precondition $a$(v) is $P$ s v))